So, now we can finally get back to the end of the chapter about natural transformations.

Man, this is more advanced than I thought.

So, the first thing we didn't finish last time would be the proof of the Yoneda Lemma.

I'm sure everyone knows what that means.

So, the Yoneda Lemma is really one of the great wonders of nature,

depending on whether you are a Platonist or not.

So, the Lemma is not even called Yoneda Lemma, it's just called Yoneda.

So, that's enough.

If the sentences you prove don't carry the name of something like the sentence of Weierstraße anymore,

then you can just call it your own name.

This says something about covariant, quantity-value functions

and their relationship to representable functions in the function category.

So, let's take a representing object, A in C.

Then the covariant homfg of A, I mean the natural transformations,

the natural transformations from covariant homfg to A to G are in the reaction with GA.

So, I have a complete overview of this first, frighteningly complex object here.

So, the corresponding parts of the bijection look like this, from left to right.

I have a natural transformation alpha and I have to think up an element of GA.

So, I'm going to think up what I can think of, namely,

I'm going to take the components of my natural transformation at A,

that's a representation from CA,A to GA, that's quite promising.

So, I have an element of GA, as soon as I find one of CA,A,

no problem, I'll take the identity.

And vice versa, let's take z, y is standard, z is not.

So, vice versa, I have an element x here and I have to think up a natural transformation.

I wrote it down last time in a complicated way, by explicitly writing down the dependence on the type,

I have written down in the style of System F.

But now the actual programming expression is hanging,

which I then don't even get from the type.

So, I'm going to write it very boldly without reference to the object,

but I'm just going to give a uniform lambda expression.

That has to be a representation from CA,B to GB, for every B,

but as I said, the definition of this representation will not be dependent on G,

because I have to represent some H, that is something from A to some B,

and I have to produce something from the type GB, very easily.

I'm going to represent GH, that's a representation from GA to GB,

and I can get something from the type GB from the existing element of GA.

So, now both directions are very simple expressions.

What I'm doing here is basically polymorph programming.

In Haskell I would do that too.

In Haskell I wouldn't explicitly make the dependence on the type,

but I would simply write this lambda expression and be satisfied with it,

that it works for every B.

So, that's it for the last time.

The proof is missing.

Can we list someone to show what it is?

The proof is, first of all, an exercise in not losing the overview.

So, which things do I have to show?

Yes?

It's a question of naturalness.